$\forall$$T$:Type, $l$:$T$ List, $i$:$\mathbb{Z}$, $j$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$l$$\parallel$}}$, $x$:$T$. $l$[$i$:=$x$][$j$] $=$ if $j$=$_{2}$$i$$\rightarrow$ $x$ else $l$[$j$] fi $\in$ $T$